Nuprl Lemma : Reffect?_wf
11,40
postcript
pdf
x1
:es_realizer{i:l}. Reffect?(
x1
)
latex
Definitions
x
,
y
,
z
,
w
,
v
.
t
(
x
;
y
;
z
;
w
;
v
)
,
x
.
t
(
x
)
,
x
,
y
,
z
,
u
,
v
,
w
.
t
(
x
;
y
;
z
;
u
;
v
;
w
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
,
y
,
z
,
w
.
t
(
x
;
y
;
z
;
w
)
,
Reffect?(
x1
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
x
(
s1
,
s2
,
s3
,
s4
,
s5
)
,
x
(
a
,
b
,
c
,
d
,
e
,
f
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
s1
,
s2
,
s3
,
s4
)
Lemmas
finite-prob-space
wf
,
fpf
wf
,
decl-type
wf
,
decl-state
wf
,
btrue
wf
,
IdLnk
wf
,
Knd
wf
,
Id
wf
,
rationals
wf
,
es
realizer
wf
,
bfalse
wf
,
bool
wf
,
es
realizer
ind
wf
origin
x,y,z,w,v. t(x;y;z;w;v), x. t(x), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z. t(x;y;z), x,y,z,w. t(x;y;z;w), Reffect?(x1), t 
T, 
x:A. B(x), x(s), x(s1,s2,s3,s4,s5), x(a,b,c,d,e,f), x(s1,s2,s3), x(s1,s2,s3,s4)